FDL - Nuprl Lemma : strong-subtype-set

Nuprl Lemma : strong-subtype-set

A, B:Type.
strong-subtype(A;B)

(

P:(A

Prop), Q:(B

Prop).

((

x:A. P(x)

Q(x))

strong-subtype({x:A| P(x) };{x:B| Q(x) }))

Definitions True, T, strong-subtype(A;B), x(s), Prop, x:A. B(x), P Q, x:A. B(x), A & B, t T